package org.xteam.sled.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.xteam.parser.runtime.AstList;
import org.xteam.parser.runtime.IErrorReporter;
import org.xteam.parser.runtime.Span;
import org.xteam.sled.ast.AbstractPattern;
import org.xteam.sled.ast.AndPattern;
import org.xteam.sled.ast.AnyPatternBinding;
import org.xteam.sled.ast.BitSpec;
import org.xteam.sled.ast.Branch;
import org.xteam.sled.ast.CheckedItem;
import org.xteam.sled.ast.Constructor;
import org.xteam.sled.ast.DefaultSledVisitor;
import org.xteam.sled.ast.Equation;
import org.xteam.sled.ast.FieldInfo;
import org.xteam.sled.ast.FieldInfoItem;
import org.xteam.sled.ast.FieldInfoSpec;
import org.xteam.sled.ast.FieldName;
import org.xteam.sled.ast.FieldSpec;
import org.xteam.sled.ast.FieldsSpec;
import org.xteam.sled.ast.GuaranteedItem;
import org.xteam.sled.ast.Ident;
import org.xteam.sled.ast.IdentOpName;
import org.xteam.sled.ast.IdentOperand;
import org.xteam.sled.ast.ListPatternBinding;
import org.xteam.sled.ast.NameBinding;
import org.xteam.sled.ast.NamesItem;
import org.xteam.sled.ast.NoiseOperand;
import org.xteam.sled.ast.OpName;
import org.xteam.sled.ast.PatternIdent;
import org.xteam.sled.ast.RelocatableSpec;
import org.xteam.sled.ast.SimplePatternBinding;
import org.xteam.sled.ast.SledFile;
import org.xteam.sled.ast.SparseItem;
import org.xteam.sled.ast.UncheckedItem;
import org.xteam.sled.model.IDisjunct;
import org.xteam.sled.model.ISequent;
import org.xteam.sled.model.LabelledPattern;
import org.xteam.sled.model.LatentPattern;
import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpCondition;
import org.xteam.sled.semantic.exp.ExpRewriter;
import org.xteam.sled.semantic.exp.ExpVar;
import org.xteam.sled.solver.EquationSolver;
import org.xteam.sled.solver.SolverResult;


public class SledToModel {

	private IErrorReporter reporter;
	private SemanticContext context;

	public SledToModel(IErrorReporter reporter) {
		this.reporter = reporter;
	}

	public SemanticContext analyse(SledFile file) {
		context = new SemanticContext(reporter);
		file.visit(new PrimaryVisitor());
		return context;
	}
	
	private void reportError(Span span, String msg) {
		reporter.reportError(span.from(), span.length(), msg);
	}
	
	private void reportWarning(Span span, String msg) {
		reporter.reportWarning(span.from(), span.length(), msg);
	}
	
	private Field projectField(IDenotable d, Span span) {
		if (d == null)
			return null;
		if (d instanceof Field) {
			return (Field) d;
		}
		reportError(span, d + " is not a field");
		return null;
	}
	
	private class PrimaryVisitor extends DefaultSledVisitor {
		
		private TokenClass currentClass;
		private Field currentField;
		
		public void visitFieldsSpec(FieldsSpec fieldsSpec) {
			int size = fieldsSpec.getSize().getValue();
			currentClass = new TokenClass(fieldsSpec.getName().getName(), size);
			for (FieldSpec fieldSpec : fieldsSpec.getFields()) {
				fieldSpec.visit(this);
			}
			context.bindUnbound(currentClass.name(), currentClass, fieldsSpec.getName().span());
			if ((size % context.pcUnitBits) != 0) {
				reportError(fieldsSpec.getSize().span(), "size of token (" + size
						+ ") must be a multiple of pc_unit_bits = " + context.pcUnitBits);
				/*for (int i = 0; i < currentClass.getFields().size(); ++i) {
					context.bindError(((Field)currentClass.getFields().get(i)).name());
				}*/
			}
			context.addTokenClass(currentClass);
		}
		
		public void visitFieldSpec(FieldSpec fieldSpec) {
			int low = fieldSpec.getLow().getValue();
			int hi = fieldSpec.getHigh() == null ? low : fieldSpec.getHigh().getValue();
			Range range = context.bitNumbering().make0LSB(currentClass.size(), new Range(low, hi+1));
			Field f = new Field(fieldSpec.getName().getName(), range, currentClass);
			if (low <= hi) {
				context.bindUnbound(fieldSpec.getName().getName(), f, fieldSpec.getName().span());
				context.bitNumbering().setUsed();
				currentClass.add(f);
		   } else {
				reportError(fieldSpec.span(), "range bounds out of order");
				context.bindUnboundError(fieldSpec.getName().getName(), fieldSpec.getName().span());
		    }
		}
		
		public void visitRelocatableSpec(RelocatableSpec relocatableSpec) {
			for (Ident ident : relocatableSpec.getVars()) {
				context.addRelocatable(ident.getName());
			}
		}
		
		public void visitBitSpec(BitSpec bitSpec) {
			if (bitSpec.getZeroInt().getValue() != 0) {
				reportError(bitSpec.getZeroInt().span(), "integer must be 0");
			}
			if (! bitSpec.getValue().getName().equals("most")
					&& ! bitSpec.getValue().getName().equals("least")) {
				reportError(bitSpec.getValue().span(), "bit spec must be 'most' or 'least'");
			} else {
				if (context.bitNumbering().isUsed()) {
					reportWarning(bitSpec.span(),
							"You change the bit numbering, but you've already used the "
							+ "old numbering ... seems like a crazy idea, but I'll do it");
				} else if (context.bitNumbering().isSet()) {
					reportWarning(bitSpec.span(),
							"You set the bit numbering twice?  On your head be it...");
				}
				context.bitNumbering().set(bitSpec.getValue().getName().equals("most"));
			}
		}
		
		public void visitFieldInfoSpec(FieldInfoSpec fieldInfoSpec) {
			for (FieldInfo info : fieldInfoSpec.getInfos()) {
				info.visit(this);
			}
		}
		
		public void visitFieldInfo(FieldInfo fieldInfo) {
			for (Ident ident : fieldInfo.getIdents()) {
				currentField = projectField(context.lookup(ident.getName(), ident.span()),
						ident.span());
				if (currentField != null) {
					for (FieldInfoItem item : fieldInfo.getItems()) {
						item.visit(this);
					}
				}
			}
		}

		public void visitCheckedItem(CheckedItem checkedItem) {
			context.setChecking(currentField, FieldInformations.CHECKED);
		}
		
		public void visitUncheckedItem(UncheckedItem uncheckedItem) {
			context.setChecking(currentField, FieldInformations.UNCHECKED);
		}
		
		public void visitGuaranteedItem(GuaranteedItem guaranteedItem) {
			context.setChecking(currentField, FieldInformations.GUARANTEED);
		}
		
		public void visitNamesItem(NamesItem namesItem) {
			int x = 0;
			Map<String, Integer> tab = new HashMap<String, Integer>();
			for (FieldName name : namesItem.getNames()) {
				if (tab.containsKey(name.getValue())) {
					reporter.reportError(name.span().from(), name.span().length(),
							"Duplicate definitions for value " + name.getValue()
							+ " of field " + currentField.name());
				} else {
					tab.put(name.getValue(), x);
				}
				++x;
			}
		    if (x != currentField.fieldmax()) {
		    	reporter.reportError(namesItem.span().from(), namesItem.span().length(),
		    			"Field " + currentField.name() + " has " + currentField.fieldmax()
		    			+ " values, but spec gave " + x + " names");
		    }
		    context.bindSpec(currentField, tab, true, namesItem.span());
		}

		public void visitSparseItem(SparseItem sparseItem) {
			Map<String, Integer> tab = new HashMap<String, Integer>();
			for (NameBinding nm : sparseItem.getBindings()) {
				// original allowed expression in semantic but not in syntax
				// (TargetWord.fromInt o insistInt o ElabExp.insistSingle) (elabInt e)
				int value = nm.getValue().getValue();
				if (value < 0 || value >= currentField.fieldmax()) {
					reportError(nm.getValue().span(),
							"Value " + value + " won't fit in field " + currentField.name());
				} else {
					if (tab.containsKey(nm.getName().getValue())) {
						reportError(nm.getName().span(),
								"Duplicate definitions for value " + nm.getName().getValue()
								+ " of field " + currentField.name());
					} else {
						tab.put(nm.getName().getValue(), value);
					}
				}
			}
			context.bindSpec(currentField, tab, false, sparseItem.span());
		}
		
		public void visitAnyPatternBinding(AnyPatternBinding anyPatternBinding) {
			PatternSemantic ps = new PatternSemantic(context);
			anyPatternBinding.getPattern().visit(ps);
			if (!ps.hasError()) {
				List<LabelledPattern> result = ps.getPatternList();
				if (result == null)
					reportError(anyPatternBinding.span(),
							"identifier list must be bound to generator");
				else if (result.size() != anyPatternBinding.getNames().size()) {
					reportError(anyPatternBinding.span(), "table has "
							+ anyPatternBinding.getNames().size()
							+ " identifiers, but RHS generates "
							+ result.size() + " patterns");
				} else {
					LabelledPattern anyPattern = null;
					for (int i = 0; i < result.size(); ++i) {
						Ident name = anyPatternBinding.getNames().get(i);
						if (!name.getName().equals("_")) {
							bindPattern(name, result.get(i));
						}
						anyPattern = anyPattern == null ? result.get(i)
								: anyPattern.or(result.get(i));
					}
					bindPattern(anyPatternBinding.getName(), anyPattern);
				}
			}
		}

		public void visitListPatternBinding(
				ListPatternBinding listPatternBinding) {
			PatternSemantic ps = new PatternSemantic(context);
			listPatternBinding.getPattern().visit(ps);
			List<LabelledPattern> result = ps.getPatternList();
			if (ps.hasError())
				return;
			if (result == null)
				reportError(listPatternBinding.span(), "identifier list must be bound to generator");
			else if (result.size() != listPatternBinding.getNames().size()) {
				reportError(listPatternBinding.span(), "table has "
						+ listPatternBinding.getNames().size() + " identifiers, but RHS generates "
						+ result.size() + " patterns");
			} else {
				
				for (int i = 0; i < result.size(); ++i) {
					Ident name = listPatternBinding.getNames().get(i);
					if (! name.getName().equals("_")) {
						bindPattern(name, result.get(i));
					}
				}
			}
			// val elabPat = gemap (Pattern.subst (simplify o eliminateInstances)) o elabPat
	        // val elabPat = Error.emap (ElabExp.gmap Patterns.purify) o elabPat
		}
		
		public void visitSimplePatternBinding(
				SimplePatternBinding simplePatternBinding) {
			PatternSemantic ps = new PatternSemantic(context);
			simplePatternBinding.getPattern().visit(ps);
			LabelledPattern result = ps.getPattern();
			if (ps.hasError())
				return;
			if (result == null)
				reportError(simplePatternBinding.span(), "generator must be bound to identifier list");
			bindPattern(simplePatternBinding.getName(), result);
		}
		
		private void bindPattern(Ident ident, LabelledPattern pattern) {
			if (pattern != null) {
				// check if pattern is "global"
				for (IDisjunct dis : pattern.getDisjuncts()) {
					if (dis.hasConditions()) {
						reportError(ident.span(),
								"top-level pattern has conditions");
						return;
					}
					for (ISequent cnsts : dis.getSequence().getElements()) {
						if (cnsts.hasInputOrLabels()) {
							reportError(ident.span(),
									"top-level pattern has inputs or labels");
							return;
						}
					}
				}
				pattern.setName(ident.getName());
			}
			context.bindUnbound(ident.getName(),
					pattern == null ? new DenotableError() : pattern, ident.span());
		}

		public void visitConstructor(Constructor aConstructor) {
			Set<String> names = new HashSet<String>();
			if (! collectOpcodeNames(aConstructor.getOpnames(), names))
				return;
			if (! collectOperandNames(aConstructor.getOperands(), names))
				return;
			List<OpcodeElement> opcodes = context.explodeOpcode(aConstructor.getOpnames());
			List<OperandSyntax> syntax = new ArrayList<OperandSyntax>();
			List<Operand> operands = new ArrayList<Operand>();
			processOperands(aConstructor.getOperands(), syntax, operands);
			if (aConstructor.getBranches().size() == 0)
				aConstructor.getBranches().add(new Branch(new Span(-1,-1), new AstList<Equation>()));
			List<BranchResult> branchResults = new ArrayList<BranchResult>();
			for (Branch branch : aConstructor.getBranches()) {
				LabelCollector collector = new LabelCollector();
				Map<String, Span> labels = collector.collect(branch.getPattern());
				Set<String> inputs = new HashSet<String>(labels.keySet());
				inputs.addAll(names);
				List<ExpCondition> equations = new ArrayList<ExpCondition>();
				if (branch.getEquations() != null) {
					for (Equation eqn : branch.getEquations()) {
						BooleanSemantic bs = new BooleanSemantic(
								new SolverContext(context));
						eqn.visit(bs);
						equations.add(bs.getExpression());
					}
				}
				EquationSolver solver = new EquationSolver();
				SolverResult result = solver.solve(inputs, equations);
				if (result.hasUnsolvables()) {
					reportError(branch.span(), "unsolvable equations");
					return;
				}
				AbstractPattern pattern = branch.getPattern();
				if (pattern == null) {
					for (String name : names) {
						PatternIdent i = new PatternIdent(branch.span(), new Ident(branch.span(), name));
						pattern = pattern == null ? i : new AndPattern(branch.span(), pattern, i);
					}
				}
				branchResults.add(new BranchResult(labels, result, pattern));
			}
			ConstructorType constype = null;
			if (aConstructor.getType() != null) {
				String name = aConstructor.getType().getName();
				IDenotable denotable = context.lookupOpt(name);
				if (denotable == null) {
					constype = new ConstructorType(name);
					context.addConstructorType(constype);
					context.bindUnbound(name, constype, aConstructor.getType().span());
				} else if (denotable instanceof ConstructorType){
					constype = (ConstructorType) denotable;
				} else {
					reportError(aConstructor.getType().span(), "must be a constructor type");
				}
			} else {
				constype = context.getInstructionConstructorType();
			}
			for (OpcodeElement opcode : opcodes) {
				System.out.println("Making: " + opcode.name());
				//f = addC, x = (constab, good), (syntax, operands), ty, branches lookup (name, rho=env)
				Map<String, IDenotable> rho = new HashMap<String, IDenotable>(opcode.env());
				for (Operand op : operands) {
					if (rho.containsKey(op.name()))
						throw new RuntimeException("duplicated name in env");
					rho.put(op.name(), op);
				}
				SubstituteVariable subs = new SubstituteVariable(rho, aConstructor.getOpnames().span());
				// val sigma = Exp.multiSubst (optmap D.projectIntE o Util.lookup rho)
				
				// elaborate branches
				List<LatentPattern> patterns = new ArrayList<LatentPattern>();
				for (BranchResult br : branchResults) {
					Map<String, IDenotable> middlerRho = new HashMap<String, IDenotable>(rho);
					for (String var : br.getValues().keySet()) {
						Exp e = br.getValues().get(var);
						middlerRho.put(var, new Temporary(subs.rewrite(e), context.optField(var)));
					}
					for (String label : br.getLabels().keySet()) {
						if (middlerRho.containsKey(label))
							reportError(br.getLabels().get(label),
									"Pattern label " + label + " collides with operand or opcode");
						else
							middlerRho.put(label, new PatternLabel(label));
					}
					// create lookup context
					PatternSemantic ps = new PatternSemantic(new ConstructorContext(context, middlerRho));
					br.getPattern().visit(ps);
					LabelledPattern p = ps.getPattern();
					if (p == null)
						reportError(br.getPattern().span(), "generating expression not permitted");
					else {
						p.addConditions(br.getConstraints());
						LatentPattern lp = p.makeLabelsPCRelative();
						System.out.println(lp);
						patterns.add(lp);
					}
				}
				context.addConstructor(new InstructionConstructor(opcode.name(), operands, constype, patterns, syntax));
			}
			
		}
		
		private class SubstituteVariable extends ExpRewriter {
			
			private Map<String, IDenotable> rho;
			private Span span;
			private Exp root;

			public SubstituteVariable(Map<String, IDenotable> rho, Span span) {
				this.rho = rho;
				this.span = span;
			}

			public void visitVar(ExpVar expVar) {
				IDenotable denotable = rho.get(expVar.name());
				if (denotable != null) {
					Exp exp = denotable.projectInt(context, span);
					if (exp != null) {
						stack.push(exp);
					} else {
						stack.push(expVar);
					}
				} else {
					stack.push(expVar);
				}
			}
		}
		
		private boolean collectOpcodeNames(AstList<OpName> opnames, Set<String> names) {
			for (OpName opName : opnames) {
				if (opName instanceof IdentOpName) {
					String name = ((IdentOpName)opName).getValue();
					if (names.contains(name)) {
						reportError(opName.span(), "duplicate name in opcode: " + name);
						return false;
					} else {
						names.add(name);
					}
				}
			}
			return true;
		}
		
		private boolean collectOperandNames(AstList<org.xteam.sled.ast.Operand> operands, Set<String> names) {
			for (org.xteam.sled.ast.Operand operand : operands) {
				if (operand instanceof IdentOperand) {
					String name = ((IdentOperand)operand).getIdent().getName();
					if (names.contains(name)) {
						reportError(((IdentOperand)operand).getIdent().span(), "duplicate name in opcode/operands: " + name);
						return false;
					} else {
						names.add(name);
					}
				}
			}
			return true;
		}
		
		private void processOperands(AstList<org.xteam.sled.ast.Operand> operands,
				List<OperandSyntax> syntax, List<Operand> inputs) {
			for (org.xteam.sled.ast.Operand operand : operands) {
				if (operand instanceof IdentOperand) {
					IdentOperand op = (IdentOperand) operand;
					String name = op.getIdent().getName();
					inputs.add(context.makeOperand(name, op.getExtend() != null, op.getIdent().span()));
					syntax.add(new IdentOperandSyntax(name, op.getExtend() != null));
				} else {
					syntax.add(new LiteralOperandSyntax(((NoiseOperand) operand).getValue()));
				}
			}
		}
		
	}

}
